|
|
Důkazy pomocí konečných automatů
Fišer, Jan ; Holub, Štěpán (vedoucí práce) ; Chvalovský, Karel (oponent)
V roce 2016 zveřejnil Hamoon Mousavi program Walnut implementující automatické dokazování vět o automatických posloupnostech. Hlavním cílem této práce bylo ukázat teoretickou funkčnost Walnutu na základě spojitosti automatických posloupností s Presburgerovou (resp. Büchiho) aritmetikou, jež je rozhodnutelnou teorií. Dalším cílem bylo s přiměřenou mírou detailnosti popsat, jak je rozhodovací procedura Walnutem doopravdy prováděna, a na závěr pak na praktických příkladech ukázat možné využití Walnutu při řešení konrétních problémů. Jedním z těchto konkrétních příkladů, jejichž řešení je v práci předvedeno, je například nalezení kritického exponentu Rudin- Shapirovy posloupnosti - tento příklad je v literatuře z roku 2003 uváděn jako otevřený problém (nicméně v současnosti se již o otevřený problém nejedná, nebot' v roce 2011 Shallit dokázal, že kritický exponent všech auto- matických posloupností je vyčíslitelný). Samotnou poslední kapitolu lze také díky tomu, že obsahuje podrobně okomentované řešené příklady, využít jako velice stručný manuál pro ty, kteří se s Walnutem setkávají poprvé a chtějí jej využít k vlastním aplikacím. 1
|
host ::
RSS.